T. Kurahashi, Y. Sato; "The finite frame property of some extensions of the pure logic of necessitation"

メモ日：2023.05.25，2023.06.15

2305.14762 The finite frame property of some extensions of the pure logic of necessitation

We study the finite frame property of some extensions of Melvin C. Fitting, V. Wiktor Marek, and Miroslaw Truszczyński's pure logic of necessitation $ \sf N. For any natural numbers $ m,n, we introduce the logic $ \mathsf{N+A}_{m,n} by adding the single axiom scheme $ □nφ→□mφ and the rule $ \frac{¬□φ}{¬□□φ} (Ros□) into $ \sf N. We prove the finite frame property of N+Am,n with respect to Fitting, Marek, and Truszczyński's relational semantics. We also prove that the Ros□ rule is necessary for the completeness of N+A0,n for n≥2

Pure Logic of Necessitation

Introduction

Pure Logic of Necessitation$ \sf N

正規様相論理から様相論理の公理K$ \mathsf{K} \equiv \Box(\varphi \to \psi) \to (\Box\varphi \to \Box\psi)を引いた非正規様相論理をPure Logic of Necessitation$ \sf Nという．

公理$ \sf 4 \equiv \Box \varphi \to \Box\Box\varphiを追加したものを$ \sf N4とする.

$ \sf N4は推移的な$ \sf Nフレームに対して有限フレーム性を持つ．

T. Kurahashi, "The provability logic of all provability predicates"などを参照．

$ \sf 4の代わりに$ \mathsf{Acc}_{m,n} \equiv \Box^n \varphi \to \Box^m \varphiを公理として追加した論理を$ \mathsf{N}\mathsf{A}_{m,n}とする．

$ (m,n)到達可能な$ \sf Nフレームに対して健全．(Sect 3)

$ n \ge 2での$ \mathsf{N}\mathsf{A}_{0,n}は$ (0,n)到達可能な$ \sf Nフレームに対して完全ではない，(Sect 4)

Rosser推論規則$ \mathrm{Ros}:\frac{\lnot\varphi}{\lnot\Box\varphi}と，その弱い亜種$ \mathrm{Ros}^\Box: \frac{\lnot\Box\varphi}{\lnot\Box\Box\varphi}を考える．

Rosser証明可能性述語の分析に用いられる．

$ \mathsf{N}\mathsf{A}_{m,n}に$ \rm Ros^\Boxを規則として追加した論理を$ \mathsf{N}^+\mathsf{A}_{m,n}とする．

$ m\ge1または$ n \leq 2の場合，$ \mathsf{N}^+\mathsf{A}_{m,n}は$ \mathsf{N}\mathsf{A}_{m,n}と一致する．

$ m=0, n\ge 2の場合，$ \mathsf{N}^+\mathsf{A}_{0,n}は真に$ \mathsf{N}\mathsf{A}_{0,n}の拡張となる．

各々の場合について証明し，$ \mathsf{N}^+\mathsf{A}_{m,n}が$ (m,n)到達可能な$ \sf Nフレームに対して健全である．

$ \mathsf{N}^+\mathsf{A}_{m,n}が$ (m,n)到達可能な$ \sf Nフレームに対して完全．(Sect5)

更に有限フレーム性も示す．

Harropの補題より(?)$ \mathsf{N}^+\mathsf{A}_{m,n}は決定可能

その他の話題(Sect6)

Def

論理式$ \varphi ::= p \mid \bot \mid \lnot\psi \mid \psi_1 \lor \psi_2 \mid \Box \psi

$ \rm MFを様相論理の論理式全ての集合とする．

$ \rm Sub(\varphi)を$ \varphiの部分論理式の集合とする．

Def. Pure Logic of Necessitation

非正規様相論理Pure Logic of Necessitationを$ \sf Nで表記して↓のように導入する．

公理

古典命題論理のトートロジー

推論規則

モーダス・ポネンス

ネセシテーション

注意

要するに公理として$ \mathsf{K} \equiv \Box(\varphi \to \psi) \to (\Box\varphi \to \Box\psi)が無いので正規様相論理ではない．

よってKripkeモデルは使えない．Pure Logic of Necessitationの擬Kripkeモデルを考える．

Def: Pure Logic of Necessitationの擬Kripkeモデル

表記

Pure Logic of Necessitationの擬Kripkeフレームを$ \sf Nフレームという．

Pure Logic of Necessitationの擬Kripkeモデルを$ \sf Nモデルという．

$ \sf Nフレームとは$ \mathcal{F} \coloneqq \lang W, \{\prec_\varphi\}_{\varphi \in \rm{MF}}\rangとする．

$ Wは非空集合．$ \prec_\varphiは全ての$ \varphi \in \rm MFに対して$ W上に定まる二項関係とする．

$ Wが有限集合のとき有限$ \sf Nフレームという．

$ \sf Nモデルとは適当な$ \sf Nフレーム$ \mathcal{F}と付値$ V:W\times \mathrm{PropVar} \to \{0,1\}による$ \mathcal{M} \coloneqq \lang \mathcal{F}, V\rangとする．

$ \sf Nモデル$ \mathcal{M} \coloneqq \lang W, \{\prec_\varphi\}_{\varphi \in \rm{MF}}, V\rang,w \in Wとして真の概念を定める．

$ w \Vdash_\mathcal{M} p \iff V(w,p) = 1

$ w \not\Vdash_\mathcal{M} \bot

$ w \Vdash_\mathcal{M} \lnot \psi \iff w \not\Vdash_\mathcal{M} \psi

$ w \Vdash_\mathcal{M} \psi_1 \lor \psi_2$ \iff$ w \Vdash_\mathcal{M} \psi_1または$ \mathcal{M},w \models \psi_2

$ w \Vdash_\mathcal{M} \Box\psi$ \iff$ w \prec_\psi w'な任意の$ w'で$ w' \Vdash_\mathcal{M} \psi

$ Vについてわざわざ言わなくて良いとき，$ \Vdash = \Vdash_\mathcal{M}となるような$ \Vdashを適当にとってきて，$ \mathcal{M} \coloneqq \lang \mathcal{F}, \Vdash \rangと書くとする．

$ \psiがある$ \sf Nモデル$ \mathcal{M} \coloneqq \lang W, \{\prec_\varphi\}_{\varphi \in \rm{MF}}, \Vdash \rangで妥当

任意の$ w \in Wについて$ w \Vdash_\mathcal{M} \varphi

$ \psiがある$ \sf Nフレーム$ \mathcal{F}で妥当

$ \mathcal{F}上の任意の$ \sf Nモデル$ \lang \mathcal{F}, \Vdash \rangで妥当であることである．

Thm: M.C.Fitting, V.W.Marek, M.Truszczyński; "The pure logic of necessitation": 3.6, 4.10

次の1~3は同値である．$ \psi \in \mathrm{MF}

1. $ \sf N \vdash \psi

2. $ \sf \psiが任意の$ \sf Nフレームで妥当

3. $ \sf \psiが任意の有限$ \sf Nフレームで妥当

Prop: M.C.Fitting, V.W.Marek, M.Truszczyński; "The pure logic of necessitation"の4.11

$ \psi \in \mathrm{MF}

$ \sf Nモデル$ \mathcal{M} \coloneqq \lang W, \{\prec_\varphi\}_{\varphi \in \rm{MF}}, V\rangと$ \mathcal{M}' \coloneqq \lang W, \{\prec'_\varphi\}_{\varphi \in \rm{MF}}, V\rang

ただし任意の$ \Box\chi \in \mathrm{Sub}(\psi)に対して$ \prec_\chi = \prec'_\chi

任意の$ w \in Wに対し，$ w \Vdash_\mathcal{M} \psi \iff w \Vdash_{\mathcal{M}'} \psi

Cor

$ \psi \in \mathrm{MF}

$ \sf Nフレーム$ \mathcal{F} \coloneqq \lang W, \{\prec_\varphi\}_{\varphi \in \rm{MF}}\rangと$ \mathcal{F}' \coloneqq \lang W, \{\prec'_\varphi\}_{\varphi \in \rm{MF}}\rang

ただし任意の$ \Box\chi \in \mathrm{Sub}(\psi)に対して$ \prec_\chi = \prec'_\chi

$ \psiが$ \mathcal{F}で妥当$ \iff$ \psiが$ \mathcal{F}'で妥当